es:ES, T:Type, eq:EqDecider(T), v:T, x:Id, e:{e:E| @loc(e)(x:T)} ,
e':{e':E| e loc e'  & (x after e') = v} .
e loc next event in [e;e'] after which x = v 
& (x after next event in [e;e'] after which x = v) = v
& e''[e,next event in [e;e'] after which x = v).((x after e'') = v) 

latex

Definitions	t.1, x. t(x), next event in [e;bound] after which x = v, @i(x:T), P  Q, P  Q, P  Q, , P  Q, A c B, t  T, e loc e' , P & Q, EqDecider(T), x:A. B(x), x:A. B(x), e'e.P(e'), x(s)
Lemmas	not wf, alle-between1 wf, existse-ge wf, es-isconst wf, event system wf, assert wf, iff wf, bool wf, Id wf, es-loc wf, es-dtype wf, es-E wf, es-vartype wf, es-le-loc, es-after wf, es-locl wf